Nuprl Lemma : intpair-less-antireflexive
11,40
postcript
pdf
y
:(
:
).
y
<
y
False
latex
Definitions
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
x
<
y
,
P
Q
,
x
:
A
B
(
x
)
,
s
=
t
,
,
,
a
<
b
,
t
T
,
P
Q
,
left
+
right
,
P
&
Q
,
False
,
!Void()
origin
y:(:
). y < y 
False y:(: ). y < y False x:A. B(x)
B(x) Q B(x)
T
Q